(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_LRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(assert (let ((e2 3))
(let ((e3 0))
(let ((e4 0))
(let ((e5 (- v1 v1)))
(let ((e6 (* v1 e3)))
(let ((e7 (- e6 e5)))
(let ((e8 (/ e4 (- e2))))
(let ((e9 (- v0 e6)))
(let ((e10 (> e7 e8)))
(let ((e11 (= e7 v0)))
(let ((e12 (<= e6 v0)))
(let ((e13 (distinct e9 e9)))
(let ((e14 (>= e5 e8)))
(let ((e15 (> e7 e6)))
(let ((e16 (> e7 v1)))
(let ((e17 (ite e13 e6 e6)))
(let ((e18 (ite e14 e8 e9)))
(let ((e19 (ite e14 e7 e18)))
(let ((e20 (ite e15 e7 v1)))
(let ((e21 (ite e10 v0 v1)))
(let ((e22 (ite e11 e21 e21)))
(let ((e23 (ite e16 e5 v1)))
(let ((e24 (ite e12 e7 e19)))
(let ((e25 (> e20 e9)))
(let ((e26 (>= e9 e17)))
(let ((e27 (<= e21 e7)))
(let ((e28 (= e17 e23)))
(let ((e29 (< e5 e6)))
(let ((e30 (< e5 v1)))
(let ((e31 (= e20 e17)))
(let ((e32 (> e5 e19)))
(let ((e33 (<= e23 e18)))
(let ((e34 (distinct v1 e20)))
(let ((e35 (distinct v0 e21)))
(let ((e36 (< v1 e22)))
(let ((e37 (> e17 e18)))
(let ((e38 (>= e6 e17)))
(let ((e39 (distinct e17 e23)))
(let ((e40 (> e7 e24)))
(let ((e41 (>= e18 v1)))
(let ((e42 (= e23 e8)))
(let ((e43 (ite e25 e34 e34)))
(let ((e44 (and e15 e42)))
(let ((e45 (not e33)))
(let ((e46 (=> e30 e16)))
(let ((e47 (not e46)))
(let ((e48 (not e12)))
(let ((e49 (and e35 e14)))
(let ((e50 (xor e39 e31)))
(let ((e51 (ite e11 e38 e38)))
(let ((e52 (= e40 e41)))
(let ((e53 (not e51)))
(let ((e54 (= e10 e26)))
(let ((e55 (or e52 e44)))
(let ((e56 (ite e45 e53 e43)))
(let ((e57 (and e49 e32)))
(let ((e58 (xor e54 e55)))
(let ((e59 (not e37)))
(let ((e60 (= e47 e36)))
(let ((e61 (or e58 e48)))
(let ((e62 (not e60)))
(let ((e63 (and e27 e27)))
(let ((e64 (=> e50 e61)))
(let ((e65 (and e13 e57)))
(let ((e66 (ite e29 e56 e63)))
(let ((e67 (ite e59 e28 e66)))
(let ((e68 (xor e65 e64)))
(let ((e69 (ite e62 e67 e62)))
(let ((e70 (= e68 e68)))
(let ((e71 (and e70 e70)))
(let ((e72 (= e71 e71)))
(let ((e73 (or e69 e69)))
(let ((e74 (=> e72 e72)))
(let ((e75 (= e74 e73)))
e75
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
